1. Field
The field of the present invention relates to verification technology of digital designs, and in particular, to a method and system for handling assertion libraries in functional verification.
2. Description of Related Art
For logic verification of digital designs, various techniques, such as formal verification, simulation and acceleration, are used. One of the verification mechanisms that are used in these techniques is Assertion Based Verification (ABV).
In ABV, assertions monitor design behavior against behavior specified in the assertion. Assertions provide a terse way to specify the behavior to be checked and are usable in the verification flow. Assertions may be written on the interface of the block being checked or on the internal signals. Assertions may specify a variety of behavior including safety assertions for specifying that something bad should not happen and liveness assertions for specifying that something good should eventually happen.
Typically, a single assertion in itself specifies only a part of the behavior. In general, to specify the behavior of a design block, a set of assertions is needed. Assertions are categorized based on whether it specifies the behavior of the inputs (or environment) or the outputs (current design under test). This bifurcation assists in making the input assertions as constraints for formal verification.
Assertions specify behavior in a variety of temporal logics. The most commonly used temporal logics are LTL (Linear-Time-Logic) and CTL (Computation Tree Logic). Assertion languages are used to specify this behavior. Some of the standard languages for assertions are IEEE 1850 PSL (Property Specification Language) and IEEE1800 SVA (System Verilog Assertions). In general, these languages provide basic constructs to specify design behavior. Design behavior is coded by a set of assertions that specify a part of the behavior.